1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Sébastien Gouëzel
5
6 Construction of a good coupling between nonempty compact metric spaces, minimizing
7 their Hausdorff distance. This construction is instrumental to study the Gromov-Hausdorff
8 distance between nonempty compact metric spaces -/
9
10 import topology.bounded_continuous_function topology.metric_space.gluing
src └──────────────────────────────────┘ └──────────────────────────┘
11 topology.metric_space.hausdorff_distance
src └──────────────────────────────────────┘
12
13 noncomputable theory
14 open_locale classical
15 open_locale topological_space
16 universes u v w
17
18 open classical lattice set function topological_space filter metric quotient
19 open bounded_continuous_function
20 open sum (inl inr)
21 set_option class.instance_max_depth 50
doc └──────────────────────┘
22
23 local attribute [instance] metric_space_sum
24
25 namespace Gromov_Hausdorff
26
27 section Gromov_Hausdorff_realized
28 /- This section shows that the Gromov-Hausdorff distance
29 is realized. For this, we consider candidate distances on the disjoint union
30 α ⊕ β of two compact nonempty metric spaces, almost realizing the Gromov-Hausdorff
31 distance, and show that they form a compact family by applying Arzela-Ascoli
32 theorem. The existence of a minimizer follows. -/
33
34 section definitions
35 variables (α : Type u) (β : Type v)
36 [metric_space α] [compact_space α] [nonempty α]
id └──────────┘ └───────────┘ └──────┘
src └──────────┘ └───────────┘ └──────┘
typ └──────────┘ └───────────┘ └──────┘
doc └──────────┘ └───────────┘
37 [metric_space β] [compact_space β] [nonempty β]
id └──────────┘ └───────────┘ └──────┘
src └──────────┘ └───────────┘ └──────┘
typ └──────────┘ └───────────┘ └──────┘
doc └──────────┘ └───────────┘
38
39 @[reducible] private def prod_space_fun : Type* := ((α ⊕ β) × (α ⊕ β)) → ℝ
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
40 @[reducible] private def Cb : Type* := bounded_continuous_function ((α ⊕ β) × (α ⊕ β)) ℝ
id └─────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────────────────┘ ┴ ┴ ┴ ┴
typ └─────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └─────────────────────────┘
41
42 private def max_var : nnreal :=
id └────┘
src └────┘
typ └────┘
doc └────┘
43 2 * ⟨diam (univ : set α), diam_nonneg⟩ + 1 + 2 * ⟨diam (univ : set β), diam_nonneg⟩
id ┴ └──┘ └──┘ └─┘ ┴ └─────────┘ ┴ ┴ ┴ └──┘ └──┘ └─┘ ┴ └─────────┘
src ┴ └──┘ └──┘ └─┘ └─────────┘ ┴ ┴ ┴ └──┘ └──┘ └─┘ └─────────┘
typ ┴ └──┘ └──┘ └─┘ ┴ └─────────┘ ┴ ┴ ┴ └──┘ └──┘ └─┘ ┴ └─────────┘
doc └──┘ └─────────┘ └──┘ └─────────┘
44
45 private lemma one_le_max_var : 1 ≤ max_var α β := calc
id ┴ └─────┘ ┴ ┴
src ┴ └─────┘
typ ┴ └─────┘ ┴ ┴
46 (1 : real) = 2 * 0 + 1 + 2 * 0 : by simp
id └──┘
src └──┘ └────
typ └──┘ └────
doc └────
txt └────
par └────
pid └
47 ... ≤ 2 * diam (univ : set α) + 1 + 2 * diam (univ : set β) :
id └──┘ └──┘ └─┘ └──┘ └──┘ └─┘
src ─┘ └──┘ └──┘ └─┘ └──┘ └──┘ └─┘
typ ─┘ └──┘ └──┘ └─┘ └──┘ └──┘ └─┘
doc ─┘ └──┘ └──┘
txt ─┘
par ─┘
pid ─┘
48 by apply_rules [add_le_add, mul_le_mul_of_nonneg_left, diam_nonneg, diam_nonneg]; norm_num
id └───────┘
src └───────────┘ └┘ └┘ └┘ └───────┘┴ └────────
typ └───────────┘ └┘ └┘ └┘ └───────┘┴ └────────
doc └───────────┘ └┘ └┘ └┘ └───────┘┴ └────────
txt └───────────┘ └┘ └┘ └┘ ┴ └────────
par └───────────┘ └┘ └┘ └┘ ┴ └────────
pid └┘ └┘ └┘ └┘ ┴ └
st └────────────────────
49
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
50 /-- The set of functions on α ⊕ β that are candidates distances to realize the
51 minimum of the Hausdorff distances between α and β in a coupling -/
52 def candidates : set (prod_space_fun α β) :=
id └─┘ └────────────┘ ┴ ┴
src └─┘ └────────────┘
typ └─┘ └────────────┘ ┴ ┴
53 {f | (((((∀x y : α, f (sum.inl x, sum.inl y) = dist x y)
id ┴┴ ┴ ┴ ┴└─────┘ ┴ └─────┘ ┴ ┴ └──┘ ┴ ┴
src ┴ ┴└─────┘ └─────┘ ┴ └──┘
typ ┴┴ ┴ ┴ ┴└─────┘ ┴ └─────┘ ┴ ┴ └──┘ ┴ ┴
54 ∧ (∀x y : β, f (sum.inr x, sum.inr y) = dist x y))
id ┴ ┴ ┴ ┴└─────┘ ┴ └─────┘ ┴ ┴ └──┘ ┴ ┴
src ┴ ┴└─────┘ └─────┘ ┴ └──┘
typ ┴ ┴ ┴ ┴└─────┘ ┴ └─────┘ ┴ ┴ └──┘ ┴ ┴
55 ∧ (∀x y, f (x, y) = f (y, x)))
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
56 ∧ (∀x y z, f (x, z) ≤ f (x, y) + f (y, z)))
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
57 ∧ (∀x, f (x, x) = 0))
id ┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴
58 ∧ (∀x y, f (x, y) ≤ max_var α β) }
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴
src ┴ ┴ ┴ └─────┘
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴
59
60 /-- Version of the set of candidates in bounded_continuous_functions, to apply
61 Arzela-Ascoli -/
62 private def candidates_b : set (Cb α β) := {f : Cb α β | f.val ∈ candidates α β}
id └─┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴└──┘ ┴ └────────┘ ┴ ┴
src └─┘ └┘ ┴ └┘ └──┘ ┴ └────────┘
typ └─┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴└──┘ ┴ └────────┘ ┴ ┴
doc └────────┘
63
64 end definitions --section
65
66 section constructions
67
68 variables {α : Type u} {β : Type v}
69 [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β]
id └──────────┘ └───────────┘ └──────┘ └──────────┘ └───────────┘ └──────┘
src └──────────┘ └───────────┘ └──────┘ └──────────┘ └───────────┘ └──────┘
typ └──────────┘ └───────────┘ └──────┘ └──────────┘ └───────────┘ └──────┘
doc └──────────┘ └───────────┘ └──────────┘ └───────────┘
70 {f : prod_space_fun α β} {x y z t : α ⊕ β}
id └────────────┘ ┴
src └────────────┘ ┴
typ └────────────┘ ┴
71 local attribute [instance, priority 10] inhabited_of_nonempty'
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
72
73 private lemma max_var_bound : dist x y ≤ max_var α β := calc
id └──┘ ┴ ┴ ┴ └─────┘ ┴ ┴
src └──┘ ┴ └─────┘
typ └──┘ ┴ ┴ ┴ └─────┘ ┴ ┴
74 dist x y ≤ diam (univ : set (α ⊕ β)) :
id └──┘ └──┘ └──┘ └─┘
src └──┘ └──┘ └──┘ └─┘
typ └──┘ └──┘ └──┘ └─┘
doc └──┘
75 dist_le_diam_of_mem (bounded_of_compact compact_univ) (mem_univ _) (mem_univ _)
id └─────────────────┘ └────────────────┘ └──────────┘ └──────┘ └──────┘
src └─────────────────┘ └────────────────┘ └──────────┘ └──────┘ └──────┘
typ └─────────────────┘ └────────────────┘ └──────────┘ └──────┘ └──────┘
doc └─────────────────┘ └────────────────┘
76 ... = diam (inl '' (univ : set α) ∪ inr '' (univ : set β)) :
id └──┘ └─┘ └──┘ └─┘ └─┘ └──┘ └─┘
src └──┘ └─┘ └──┘ └─┘ └─┘ └──┘ └─┘
typ └──┘ └─┘ └──┘ └─┘ └─┘ └──┘ └─┘
doc └──┘
77 by apply congr_arg; ext x y z; cases x; simp [mem_univ, mem_range_self]
id └──────┘ └────────────┘
src └────┘ └───────┘ └────┘ └────┘└──────┘└┘└────────────┘└─
typ └────┘ └───────┘ └────┘ └────┘└──────┘└┘└────────────┘└─
doc └────┘ └───────┘ └────┘ └────┘ └┘ └─
txt └────┘ └───────┘ └────┘ └────┘ └┘ └─
par └────┘ └───────┘ └────┘ └────┘ └┘ └─
pid ┴ └────┘ ┴ ┴┴ └┘ ┴└
st └─────────────────────────
78 ... ≤ diam (inl '' (univ : set α)) + dist (inl (default α)) (inr (default β)) + diam (inr '' (univ : set β)) :
id └──┘ └─┘ └┘ └──┘ └─┘ ┴ ┴ └──┘ └─┘ └─────┘ ┴ └─┘ └─────┘ ┴ ┴ └──┘ └─┘ └┘ └──┘ └─┘ ┴
src ─┘ └──┘ └─┘ └┘ └──┘ └─┘ ┴ └──┘ └─┘ └─────┘ └─┘ └─────┘ ┴ └──┘ └─┘ └┘ └──┘ └─┘
typ ─┘ └──┘ └─┘ └┘ └──┘ └─┘ ┴ ┴ └──┘ └─┘ └─────┘ ┴ └─┘ └─────┘ ┴ ┴ └──┘ └─┘ └┘ └──┘ └─┘ ┴
doc ─┘ └──┘ └──┘
txt ─┘
par ─┘
pid ─┘
st ─┘
79 diam_union (mem_image_of_mem _ (mem_univ _)) (mem_image_of_mem _ (mem_univ _))
id └────────┘ └──────────────┘ └──────┘ └──────────────┘ └──────┘
src └────────┘ └──────────────┘ └──────┘ └──────────────┘ └──────┘
typ └────────┘ └──────────────┘ └──────┘ └──────────────┘ └──────┘
doc └────────┘
80 ... = diam (univ : set α) + (dist (default α) (default α) + 1 + dist (default β) (default β)) + diam (univ : set β) :
id └──┘ └──┘ └─┘ ┴ ┴ └──┘ └─────┘ ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴ └─────┘ ┴ ┴ └──┘ └──┘ └─┘ ┴
src └──┘ └──┘ └─┘ ┴ └──┘ └─────┘ └─────┘ ┴ ┴ └──┘ └─────┘ └─────┘ ┴ └──┘ └──┘ └─┘
typ └──┘ └──┘ └─┘ ┴ ┴ └──┘ └─────┘ ┴ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴ └─────┘ ┴ ┴ └──┘ └──┘ └─┘ ┴
doc └──┘ └──┘
81 by { rw [isometry.diam_image isometry_on_inl, isometry.diam_image isometry_on_inr], refl }
id └─────────────────┘ └─────────────┘ └─────────────────┘ └─────────────┘
src └──┘└─────────────────┘┴└─────────────┘└┘└─────────────────┘┴└─────────────┘┴ └───┘
typ └──┘└─────────────────┘┴└─────────────┘└┘└─────────────────┘┴└─────────────┘┴ └───┘
doc └──┘└─────────────────┘┴└─────────────┘└┘└─────────────────┘┴└─────────────┘┴ └───┘
txt └──┘ ┴ └┘ ┴ ┴ └───┘
par └──┘ ┴ └┘ ┴ ┴ └───┘
pid └┘ ┴ └┘ ┴ ┴ ┴
st └────────────────────────────────────────┘└───────────────────────────────────┘└──────┘└┘
82 ... = 1 * diam (univ : set α) + 1 + 1 * diam (univ : set β) : by simp
id ┴ └──┘ └──┘ └─┘ ┴ ┴ ┴ ┴ └──┘ └──┘ └─┘ ┴
src ┴ └──┘ └──┘ └─┘ ┴ ┴ ┴ └──┘ └──┘ └─┘ └────
typ ┴ └──┘ └──┘ └─┘ ┴ ┴ ┴ ┴ └──┘ └──┘ └─┘ ┴ └────
doc └──┘ └──┘ └────
txt └────
par └────
pid └
st └─────
83 ... ≤ 2 * diam (univ : set α) + 1 + 2 * diam (univ : set β) :
id ┴ └──┘ └──┘ └─┘ ┴ ┴ ┴ ┴ └──┘ └──┘ └─┘ ┴
src ─┘ ┴ └──┘ └──┘ └─┘ ┴ ┴ ┴ └──┘ └──┘ └─┘
typ ─┘ ┴ └──┘ └──┘ └─┘ ┴ ┴ ┴ ┴ └──┘ └──┘ └─┘ ┴
doc ─┘ └──┘ └──┘
txt ─┘
par ─┘
pid ─┘
st ─┘
84 begin
st └─────
85 apply_rules [add_le_add, mul_le_mul_of_nonneg_right, diam_nonneg, diam_nonneg, le_refl],
id └────────┘ └────────────────────────┘ └─────────┘ └─────────┘ └─────┘
src └───────────┘└────────┘└┘└────────────────────────┘└┘└─────────┘└┘└─────────┘└┘└─────┘┴
typ └───────────┘└────────┘└┘└────────────────────────┘└┘└─────────┘└┘└─────────┘└┘└─────┘┴
doc └───────────┘ └┘ └┘└─────────┘└┘└─────────┘└┘ ┴
txt └───────────┘ └┘ └┘ └┘ └┘ ┴
par └───────────┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
86 norm_num, norm_num
src └──────┘ └────────
typ └──────┘ └────────
doc └──────┘ └────────
txt └──────┘ └────────
par └──────┘ └────────
pid └
st ───────────┘└──────────
87 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
88
89 private lemma candidates_symm (fA : f ∈ candidates α β) : f (x, y) = f (y ,x) := fA.1.1.1.2 x y
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴
src ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └┘┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘
90
91 private lemma candidates_triangle (fA : f ∈ candidates α β) : f (x, z) ≤ f (x, y) + f (y, z) :=
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
doc └────────┘
92 fA.1.1.2 x y z
id └┘┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ └┘┴ ┴ ┴ ┴ ┴ ┴
93
94 private lemma candidates_refl (fA : f ∈ candidates α β) : f (x, x) = 0 := fA.1.2 x
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └┘┴ ┴ ┴
src ┴ └────────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └┘┴ ┴ ┴
doc └────────┘
95
96 private lemma candidates_nonneg (fA : f ∈ candidates α β) : 0 ≤ f (x, y) :=
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ └────────┘ ┴ ┴
typ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴
doc └────────┘
97 begin
st └─────
98 have : 0 ≤ 2 * f (x, y) := calc
id ┴ ┴ ┴ ┴┴ ┴
src └───────┘┴└─┘┴┴ ┴┴ └┘ └───┘ └
typ └───────┘┴└─┘┴┴┴┴┴┴└┘┴└───┘ └
doc └───────┘ └─┘ ┴ ┴ └┘ └───┘ └
txt └───────┘ └─┘ ┴ ┴ └┘ └───┘ └
par └───────┘ └─┘ ┴ ┴ └┘ └───┘ └
pid └───┘└──┘ └─┘ ┴ ┴ └┘ ┴└──┘ └
st ──────────────────────────────────
99 0 = f (x, x) : (candidates_refl fA).symm
id ┴ ┴ └─────────────┘
src ─────┘ ┴ ┴ └┘ └──┘ └─────────────┘┴ └──────
typ ─────┘ ┴┴┴ └┘┴└──┘ └─────────────┘┴ └──────
doc ─────┘ ┴ ┴ └┘ └──┘ ┴ └──────
txt ─────┘ ┴ ┴ └┘ └──┘ ┴ └──────
par ─────┘ ┴ ┴ └┘ └──┘ ┴ └──────
pid ─────┘ ┴ ┴ └┘ └──┘ ┴ └──────
st ─────────────────────────────────────────────
100 ... ≤ f (x, y) + f (y, x) : candidates_triangle fA
id ┴ └─────────────────┘ └┘
src ───────┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └──┘└─────────────────┘┴ └
typ ───────┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴└┘ └──┘└─────────────────┘┴└┘└
doc ───────┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └──┘ ┴ └
txt ───────┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └──┘ ┴ └
par ───────┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └──┘ ┴ └
pid ───────┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └──┘ ┴ └
st ───────────────────────────────────────────────────────
101 ... = f (x, y) + f (x, y) : by rw [candidates_symm fA]
id ┴ └─────────────┘ └┘
src ───────┘ ┴ ┴ └┘ └┘┴┴ ┴ └┘ └──┘ ┴└──┘└─────────────┘┴ └─
typ ───────┘ ┴ ┴ └┘ └┘┴┴ ┴ └┘ └──┘ ┴└──┘└─────────────┘┴└┘└─
doc ───────┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └──┘ ┴└──┘ ┴ └─
txt ───────┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └──┘ ┴└──┘ ┴ └─
par ───────┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └──┘ ┴└──┘ ┴ └─
pid ───────┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └──┘ └───┘ ┴ └─
st ─────────────────────────────────┘└─────────────────────┘┴└
102 ... = 2 * f (x, y) : by ring,
src ───┘└──┘ └─┘ ┴ ┴ └┘ └──┘ ┴└──┘
typ ───┘└──┘ └─┘ ┴ ┴ └┘ └──┘ ┴└──┘
doc ───┘└──┘ └─┘ ┴ ┴ └┘ └──┘ ┴└──┘
txt ───┘└──┘ └─┘ ┴ ┴ └┘ └──┘ ┴└──┘
par ───┘└──┘ └─┘ ┴ ┴ └┘ └──┘ ┴└──┘
pid ───────┘ └─┘ ┴ ┴ └┘ └──┘ └───┘
st ───┘└─────────────────────┘└───┘
103 by linarith
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴
104 end
st └─┘
105
106 private lemma candidates_dist_inl (fA : f ∈ candidates α β) (x y: α) : f (inl x, inl y) = dist x y :=
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴└─┘ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴
src ┴ └────────┘ ┴└─┘ └─┘ ┴ └──┘
typ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴└─┘ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴
doc └────────┘
107 fA.1.1.1.1.1 x y
id └┘┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴
108
109 private lemma candidates_dist_inr (fA : f ∈ candidates α β) (x y : β) : f (inr x, inr y) = dist x y :=
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴└─┘ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴
src ┴ └────────┘ ┴└─┘ └─┘ ┴ └──┘
typ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴└─┘ ┴ └─┘ ┴ ┴ └──┘ ┴ ┴
doc └────────┘
110 fA.1.1.1.1.2 x y
id └┘┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ └┘┴ ┴ ┴ ┴ ┴ ┴ ┴
111
112 private lemma candidates_le_max_var (fA : f ∈ candidates α β) : f (x, y) ≤ max_var α β :=
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴
src ┴ └────────┘ ┴ ┴ └─────┘
typ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴
doc └────────┘
113 fA.2 x y
id └┘┴ ┴ ┴
src ┴
typ └┘┴ ┴ ┴
114
115 /-- candidates are bounded by max_var α β -/
116 private lemma candidates_dist_bound (fA : f ∈ candidates α β) :
id ┴ ┴ └────────┘ ┴ ┴
src ┴ └────────┘
typ ┴ ┴ └────────┘ ┴ ┴
doc └────────┘
117 ∀ {x y : α ⊕ β}, f (x, y) ≤ max_var α β * dist x y
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴
src ┴ ┴ ┴ └─────┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴
118 | (inl x) (inl y) := calc
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
119 f (inl x, inl y) = dist x y : candidates_dist_inl fA x y
id ┴ ┴└─┘ └─┘ └──┘ └─────────────────┘ └┘
src ┴└─┘ └─┘ └──┘ └─────────────────┘
typ ┴ ┴└─┘ └─┘ └──┘ └─────────────────┘ └┘
120 ... = dist (inl x) (inl y) : by { rw @sum.dist_eq α β, refl }
id └──┘ └─┘ └─┘ └─────────┘ ┴ ┴
src └──┘ └─┘ └─┘ └─┘ └─────────┘┴ ┴ └───┘
typ └──┘ └─┘ └─┘ └─┘ └─────────┘┴┴┴┴ └───┘
doc └─┘ ┴ ┴ └───┘
txt └─┘ ┴ ┴ └───┘
par └─┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴
st └────────────────────┘└─────┘└┘
121 ... = 1 * dist (inl x) (inl y) : by simp
id ┴ └──┘ └─┘ └─┘
src ┴ └──┘ └─┘ └─┘ └────
typ ┴ └──┘ └─┘ └─┘ └────
doc └────
txt └────
par └────
pid └
st └─────
122 ... ≤ max_var α β * dist (inl x) (inl y) :
id └─────┘ ┴ ┴ ┴ └──┘ └─┘ └─┘
src ───┘ └─────┘ ┴ └──┘ └─┘ └─┘
typ ───┘ └─────┘ ┴ ┴ ┴ └──┘ └─┘ └─┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘
123 mul_le_mul_of_nonneg_right (one_le_max_var α β) dist_nonneg
id └────────────────────────┘ └────────────┘ ┴ ┴ └─────────┘
src └────────────────────────┘ └────────────┘ └─────────┘
typ └────────────────────────┘ └────────────┘ ┴ ┴ └─────────┘
124 | (inl x) (inr y) := calc
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
125 f (inl x, inr y) ≤ max_var α β : candidates_le_max_var fA
id ┴ ┴└─┘ └─┘ └─────┘ ┴ ┴ └───────────────────┘ └┘
src ┴└─┘ └─┘ └─────┘ └───────────────────┘
typ ┴ ┴└─┘ └─┘ └─────┘ ┴ ┴ └───────────────────┘ └┘
126 ... = max_var α β * 1 : by simp
id └─────┘ ┴ ┴ ┴
src └─────┘ ┴ └────
typ └─────┘ ┴ ┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
127 ... ≤ max_var α β * dist (inl x) (inr y) :
id └─────┘ ┴ ┴ ┴ └──┘ └─┘ └─┘
src ───┘ └─────┘ ┴ └──┘ └─┘ └─┘
typ ───┘ └─────┘ ┴ ┴ ┴ └──┘ └─┘ └─┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘
128 mul_le_mul_of_nonneg_left sum.one_dist_le (le_trans (zero_le_one) (one_le_max_var α β))
id └───────────────────────┘ └─────────────┘ └──────┘ └─────────┘ └────────────┘ ┴ ┴
src └───────────────────────┘ └─────────────┘ └──────┘ └─────────┘ └────────────┘
typ └───────────────────────┘ └─────────────┘ └──────┘ └─────────┘ └────────────┘ ┴ ┴
129 | (inr x) (inl y) := calc
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
130 f (inr x, inl y) ≤ max_var α β : candidates_le_max_var fA
id ┴ ┴└─┘ └─┘ └─────┘ ┴ ┴ └───────────────────┘ └┘
src ┴└─┘ └─┘ └─────┘ └───────────────────┘
typ ┴ ┴└─┘ └─┘ └─────┘ ┴ ┴ └───────────────────┘ └┘
131 ... = max_var α β * 1 : by simp
id └─────┘ ┴ ┴ ┴
src └─────┘ ┴ └────
typ └─────┘ ┴ ┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
132 ... ≤ max_var α β * dist (inl x) (inr y) :
id └─────┘ ┴ ┴ ┴ └──┘ └─┘ └─┘
src ───┘ └─────┘ ┴ └──┘ └─┘ └─┘
typ ───┘ └─────┘ ┴ ┴ ┴ └──┘ └─┘ └─┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘
133 mul_le_mul_of_nonneg_left sum.one_dist_le (le_trans (zero_le_one) (one_le_max_var α β))
id └───────────────────────┘ └─────────────┘ └──────┘ └─────────┘ └────────────┘ ┴ ┴
src └───────────────────────┘ └─────────────┘ └──────┘ └─────────┘ └────────────┘
typ └───────────────────────┘ └─────────────┘ └──────┘ └─────────┘ └────────────┘ ┴ ┴
134 | (inr x) (inr y) := calc
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
135 f (inr x, inr y) = dist x y : candidates_dist_inr fA x y
id ┴ ┴└─┘ └─┘ └──┘ └─────────────────┘ └┘
src ┴└─┘ └─┘ └──┘ └─────────────────┘
typ ┴ ┴└─┘ └─┘ └──┘ └─────────────────┘ └┘
136 ... = dist (inr x) (inr y) : by { rw @sum.dist_eq α β, refl }
id └──┘ └─┘ └─┘ └─────────┘ ┴ ┴
src └──┘ └─┘ └─┘ └─┘ └─────────┘┴ ┴ └───┘
typ └──┘ └─┘ └─┘ └─┘ └─────────┘┴┴┴┴ └───┘
doc └─┘ ┴ ┴ └───┘
txt └─┘ ┴ ┴ └───┘
par └─┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴
st └────────────────────┘└─────┘└┘
137 ... = 1 * dist (inr x) (inr y) : by simp
id ┴ └──┘ └─┘ └─┘
src ┴ └──┘ └─┘ └─┘ └────
typ ┴ └──┘ └─┘ └─┘ └────
doc └────
txt └────
par └────
pid └
st └─────
138 ... ≤ max_var α β * dist (inr x) (inr y) :
id └─────┘ ┴ ┴ ┴ └──┘ └─┘ └─┘
src ───┘ └─────┘ ┴ └──┘ └─┘ └─┘
typ ───┘ └─────┘ ┴ ┴ ┴ └──┘ └─┘ └─┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘
139 mul_le_mul_of_nonneg_right (one_le_max_var α β) dist_nonneg
id └────────────────────────┘ └────────────┘ ┴ ┴ └─────────┘
src └────────────────────────┘ └────────────┘ └─────────┘
typ └────────────────────────┘ └────────────┘ ┴ ┴ └─────────┘
140
141 /-- Technical lemma to prove that candidates are Lipschitz -/
142 private lemma candidates_lipschitz_aux (fA : f ∈ candidates α β) : f (x, y) - f (z, t) ≤ 2 * max_var α β * dist (x, y) (z, t) :=
id ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴┴ ┴
src ┴ └────────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴
typ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴┴ ┴
doc └────────┘
143 calc
144 f (x, y) - f(z, t) ≤ f (x, t) + f (t, y) - f (z, t) : add_le_add_right (candidates_triangle fA) _
id ┴ ┴┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └──────────────┘ └─────────────────┘ └┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────┘ └─────────────────┘
typ ┴ ┴┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └──────────────┘ └─────────────────┘ └┘
145 ... ≤ (f (x, z) + f (z, t) + f(t, y)) - f (z, t) :
id ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴
146 add_le_add_right (add_le_add_right (candidates_triangle fA) _ ) _
id └──────────────┘ └──────────────┘ └─────────────────┘ └┘
src └──────────────┘ └──────────────┘ └─────────────────┘
typ └──────────────┘ └──────────────┘ └─────────────────┘ └┘
147 ... = f (x, z) + f (t, y) : by simp
id ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ └────
typ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
148 ... ≤ max_var α β * dist x z + max_var α β * dist t y :
id └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴
src ─┘ └─────┘ ┴ └──┘ ┴ └─────┘ ┴ └──┘
typ ─┘ └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
149 add_le_add (candidates_dist_bound fA) (candidates_dist_bound fA)
id └────────┘ └───────────────────┘ └┘ └───────────────────┘ └┘
src └────────┘ └───────────────────┘ └───────────────────┘
typ └────────┘ └───────────────────┘ └┘ └───────────────────┘ └┘
doc └───────────────────┘ └───────────────────┘
150 ... ≤ max_var α β * max (dist x z) (dist t y) + max_var α β * max (dist x z) (dist t y) :
id └─────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └──┘ ┴ ┴
src └─────┘ ┴ └─┘ └──┘ └──┘ ┴ └─────┘ ┴ └─┘ └──┘ └──┘
typ └─────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └──┘ ┴ ┴
151 begin
st └─────
152 apply add_le_add,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
153 apply mul_le_mul_of_nonneg_left (le_max_left (dist x z) (dist t y)) (le_trans zero_le_one (one_le_max_var α β)),
id └───────────────────────┘ └─────────┘ ┴ ┴ └──┘ ┴ ┴ └──────┘ └─────────┘ └────────────┘ ┴ ┴
src └────┘└───────────────────────┘┴ └─────────┘┴ ┴ ┴ └┘ └──┘┴ ┴ └─┘ └──────┘┴└─────────┘┴ └────────────┘┴ ┴ └┘
typ └────┘└───────────────────────┘┴ └─────────┘┴ ┴┴┴┴└┘ └──┘┴┴┴┴└─┘ └──────┘┴└─────────┘┴ └────────────┘┴┴┴┴└┘
doc └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
154 apply mul_le_mul_of_nonneg_left (le_max_right (dist x z) (dist t y)) (le_trans zero_le_one (one_le_max_var α β)),
id └───────────────────────┘ └──────────┘ ┴ ┴ └──┘ ┴ ┴ └──────┘ └─────────┘ └────────────┘ ┴ ┴
src └────┘└───────────────────────┘┴ └──────────┘┴ ┴ ┴ └┘ └──┘┴ ┴ └─┘ └──────┘┴└─────────┘┴ └────────────┘┴ ┴ └┘
typ └────┘└───────────────────────┘┴ └──────────┘┴ ┴┴┴┴└┘ └──┘┴┴┴┴└─┘ └──────┘┴└─────────┘┴ └────────────┘┴┴┴┴└┘
doc └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
155 end
st ────┘
156 ... = 2 * max_var α β * max (dist x z) (dist y t) :
id ┴ └─────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └──┘ ┴ ┴
src ┴ └─────┘ ┴ └─┘ └──┘ └──┘
typ ┴ └─────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └──┘ ┴ ┴
157 by { simp [dist_comm], ring }
id └───────┘
src └────┘└───────┘┴ └───┘
typ └────┘└───────┘┴ └───┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid ┴┴ ┴ ┴
st └─────────────────┘└─────┘└┘
158 ... = 2 * max_var α β * dist (x, y) (z, t) : by refl
id ┴ └─────┘ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴┴ ┴
src ┴ └─────┘ ┴ └──┘ ┴ ┴ └────
typ ┴ └─────┘ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
159
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
160 /-- Candidates are Lipschitz -/
161 private lemma candidates_lipschitz (fA : f ∈ candidates α β) :
id ┴ ┴ └────────┘ ┴ ┴
src ┴ └────────┘
typ ┴ ┴ └────────┘ ┴ ┴
doc └────────┘
162 lipschitz_with (2 * max_var α β) f :=
id └────────────┘ ┴ └─────┘ ┴ ┴ ┴
src └────────────┘ ┴ └─────┘
typ └────────────┘ ┴ └─────┘ ┴ ┴ ┴
doc └────────────┘
163 begin
st └─────
164 rintros ⟨x, y⟩ ⟨z, t⟩,
src └───────────────────┘
typ └───────────────────┘
doc └───────────────────┘
txt └───────────────────┘
par └───────────────────┘
pid └────────────┘
st ──────────────────────┘└─
165 rw real.dist_eq,
id └──────────┘
src └─┘└──────────┘
typ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────┘└─
166 apply abs_le_of_le_of_neg_le,
id └────────────────────┘
src └────┘└────────────────────┘
typ └────┘└────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└─
167 { exact candidates_lipschitz_aux fA },
id └──────────────────────┘ └┘
src └────┘└──────────────────────┘┴ ┴
typ └────┘└──────────────────────┘┴└┘┴
doc └────┘└──────────────────────┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───┘└────────────────────────────────┘└┘└
168 { have : -(f (x, y) - f (z, t)) = f (z, t) - f (x, y), by ring,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴
src └─────┘┴ ┴ └┘ └┘┴┴ ┴ └┘ └─┘┴┴ ┴ └┘ └┘ ┴ ┴┴ └┘ ┴ └──┘
typ └─────┘┴ ┴ └┘ └┘┴┴ ┴ └┘ └─┘┴┴ ┴ ┴└┘┴└┘ ┴┴┴┴┴└┘┴┴ └──┘
doc └─────┘ ┴ └┘ └┘ ┴ ┴ └┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └──┘
txt └─────┘ ┴ └┘ └┘ ┴ ┴ └┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └──┘
par └─────┘ ┴ └┘ └┘ ┴ ┴ └┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └──┘
pid └───┘└┘ ┴ └┘ └┘ ┴ ┴ └┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴
st ──────────────────────────────────────────────────────┘ └─
169 rw [this, dist_comm],
id └──┘ └───────┘
src └──┘ └┘└───────┘┴
typ └──┘└──┘└┘└───────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────┘└─────────┘└──
170 exact candidates_lipschitz_aux fA }
id └──────────────────────┘ └┘
src └────┘└──────────────────────┘┴ ┴
typ └────┘└──────────────────────┘┴└┘┴
doc └────┘└──────────────────────┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────────────────────┘└─
171 end
st ──┘
172
173 /-- candidates give rise to elements of bounded_continuous_functions -/
174 def candidates_b_of_candidates (f : prod_space_fun α β) (fA : f ∈ candidates α β) : Cb α β :=
id └────────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴ ┴
src └────────────┘ ┴ └────────┘ └┘
typ └────────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴ ┴
doc └────────┘
175 bounded_continuous_function.mk_of_compact f (candidates_lipschitz fA).to_continuous
id └───────────────────────────────────────┘ ┴ └──────────────────┘ └┘ └───────────┘
src └───────────────────────────────────────┘ └──────────────────┘ └───────────┘
typ └───────────────────────────────────────┘ ┴ └──────────────────┘ └┘ └───────────┘
doc └───────────────────────────────────────┘ └──────────────────┘ └───────────┘
176
177 lemma candidates_b_of_candidates_mem (f : prod_space_fun α β) (fA : f ∈ candidates α β) :
id └────────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
src └────────────┘ ┴ └────────┘
typ └────────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴
doc └────────┘
178 candidates_b_of_candidates f fA ∈ candidates_b α β := fA
id └────────────────────────┘ ┴ └┘ ┴ └──────────┘ ┴ ┴ └┘
src └────────────────────────┘ ┴ └──────────┘
typ └────────────────────────┘ ┴ └┘ ┴ └──────────┘ ┴ ┴ └┘
doc └────────────────────────┘ └──────────┘
179
180 /-- The distance on α ⊕ β is a candidate -/
181 private lemma dist_mem_candidates : (λp : (α ⊕ β) × (α ⊕ β), dist p.1 p.2) ∈ candidates α β :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴ ┴┴ ┴ └────────┘ ┴ ┴
src ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴ ┴┴ ┴ └────────┘ ┴ ┴
doc └────────┘
182 begin
st └─────
183 simp only [candidates, dist_comm, forall_const, and_true, add_comm, eq_self_iff_true,
id └────────┘ └───────┘ └──────────┘ └──────┘ └──────┘ └──────────────┘
src └─────────┘└────────┘└┘└───────┘└┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└─
typ └─────────┘└────────┘└┘└───────┘└┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└─
doc └─────────┘└────────┘└┘ └┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ └─
st ────────────────────────────────────────────────────────────────────────────────────────
184 and_self, sum.forall, set.mem_set_of_eq, dist_self],
id └──────┘ └────────┘ └───────────────┘ └───────┘
src ────────────┘└──────┘└┘└────────┘└┘└───────────────┘└┘└───────┘┴
typ ────────────┘└──────┘└┘└────────┘└┘└───────────────┘└┘└───────┘┴
doc ────────────┘ └┘ └┘ └┘ ┴
txt ────────────┘ └┘ └┘ └┘ ┴
par ────────────┘ └┘ └┘ └┘ ┴
pid ────────────┘ └┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────┘└─
185 repeat { split
src └───────┘└─────
typ └───────┘└─────
doc └───────┘└─────
txt └───────┘└─────
par └───────┘└─────
pid └────────
st ─────────────────
186 <|> exact (λa y z, dist_triangle_left _ _ _)
id └────────────────┘
src ───┘└──┘└────┘ └─────┘└────────────────┘└───────
typ ───┘└──┘└────┘ └─────┘└────────────────┘└───────
doc ───┘└──┘└────┘ └─────┘ └───────
txt ───┘└──┘└────┘ └─────┘ └───────
par ───┘└──┘└────┘ └─────┘ └───────
pid ─────────────┘ └─────┘ └───────
st ─────────────────────────────────────────────────
187 <|> exact (λx y, by refl)
src ───┘└──┘└────┘ └───┘ ┴└──┘└─
typ ───┘└──┘└────┘ └───┘ ┴└──┘└─
doc ───┘└──┘└────┘ └───┘ ┴└──┘└─
txt ───┘└──┘└────┘ └───┘ ┴└──┘└─
par ───┘└──┘└────┘ └───┘ ┴└──┘└─
pid ─────────────┘ └───┘ └──────
st ──────────────────────┘└───┘└─
188 <|> exact (λx y, max_var_bound) }
id └───────────┘
src ───┘└──┘└────┘ └───┘└───────────┘└┘└┘
typ ───┘└──┘└────┘ └───┘└───────────┘└┘└┘
doc ───┘└──┘└────┘ └───┘ └┘└┘
txt ───┘└──┘└────┘ └───┘ └┘└┘
par ───┘└──┘└────┘ └───┘ └┘└┘
pid ─────────────┘ └───┘ └─┘┴
st ───────────────────────────────────┘┴┴
189 end
st └─┘
190
191 def candidates_b_dist (α : Type u) (β : Type v) [metric_space α] [compact_space α] [inhabited α]
id └──────────┘ ┴ └───────────┘ ┴ └───────┘ ┴
src └──────────┘ └───────────┘ └───────┘
typ └──────────┘ ┴ └───────────┘ ┴ └───────┘ ┴
doc └──────────┘ └───────────┘
192 [metric_space β] [compact_space β] [inhabited β] : Cb α β := candidates_b_of_candidates _ dist_mem_candidates
id └──────────┘ ┴ └───────────┘ ┴ └───────┘ ┴ └┘ ┴ ┴ └────────────────────────┘ └─────────────────┘
src └──────────┘ └───────────┘ └───────┘ └┘ └────────────────────────┘ └─────────────────┘
typ └──────────┘ ┴ └───────────┘ ┴ └───────┘ ┴ └┘ ┴ ┴ └────────────────────────┘ └─────────────────┘
doc └──────────┘ └───────────┘ └────────────────────────┘ └─────────────────┘
193
194 lemma candidates_b_dist_mem_candidates_b : candidates_b_dist α β ∈ candidates_b α β :=
id └───────────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴
src └───────────────┘ ┴ └──────────┘
typ └───────────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘
195 candidates_b_of_candidates_mem _ _
id └────────────────────────────┘
src └────────────────────────────┘
typ └────────────────────────────┘
196
197 private lemma candidates_b_nonempty : (candidates_b α β).nonempty :=
id └──────────┘ ┴ ┴ └──────┘
src └──────────┘ └──────┘
typ └──────────┘ ┴ ┴ └──────┘
doc └──────────┘ └──────┘
198 ⟨_, candidates_b_dist_mem_candidates_b⟩
id └────────────────────────────────┘
src └────────────────────────────────┘
typ └────────────────────────────────┘
199
200 /-- To apply Arzela-Ascoli, we need to check that the set of candidates is closed and equicontinuous.
201 Equicontinuity follows from the Lipschitz control, we check closedness -/
202 private lemma closed_candidates_b : is_closed (candidates_b α β) :=
id └───────┘ └──────────┘ ┴ ┴
src └───────┘ └──────────┘
typ └───────┘ └──────────┘ ┴ ┴
doc └───────┘ └──────────┘
203 begin
st └─────
204 have I1 : ∀x y, is_closed {f : Cb α β | f (inl x, inl y) = dist x y} :=
id └───────┘ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └──┘
src └────────┘ └─┘ ┴└───────┘┴┴└──┘└┘┴ ┴ └─┘ ┴┴ ┴ └┘└─┘┴ └┘┴┴└──┘┴ ┴ └────
typ └────────┘ └─┘ ┴└───────┘┴┴└──┘└┘┴┴┴┴└─┘ ┴┴ ┴ └┘└─┘┴ └┘┴┴└──┘┴ ┴ └────
doc └────────┘ └─┘ ┴└───────┘┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └────
txt └────────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └────
par └────────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └────
pid └─────┘└─┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴└───
st ──────────────────────────────────────────────────────────────────────────
205 λx y, is_closed_eq continuous_evalx continuous_const,
id └──────────┘ └──────────────┘ └──────────────┘
src ───┘ └───┘└──────────┘┴└──────────────┘┴└──────────────┘
typ ───┘ └───┘└──────────┘┴└──────────────┘┴└──────────────┘
doc ───┘ └───┘ ┴└──────────────┘┴
txt ───┘ └───┘ ┴ ┴
par ───┘ └───┘ ┴ ┴
pid ───┘ └───┘ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
206 have I2 : ∀x y, is_closed {f : Cb α β | f (inr x, inr y) = dist x y } :=
id └───────┘ ┴ └┘ ┴ ┴ ┴ └─┘ └──┘
src └────────┘ └─┘ ┴└───────┘┴┴└──┘└┘┴ ┴ └─┘ ┴┴ ┴ └┘└─┘┴ └┘ ┴└──┘┴ ┴ └─────
typ └────────┘ └─┘ ┴└───────┘┴┴└──┘└┘┴┴┴┴└─┘ ┴┴ ┴ └┘└─┘┴ └┘ ┴└──┘┴ ┴ └─────
doc └────────┘ └─┘ ┴└───────┘┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─────
txt └────────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─────
par └────────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─────
pid └─────┘└─┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘└───
st ───────────────────────────────────────────────────────────────────────────
207 λx y, is_closed_eq continuous_evalx continuous_const,
id └──────────┘ └──────────────┘ └──────────────┘
src ───┘ └───┘└──────────┘┴└──────────────┘┴└──────────────┘
typ ───┘ └───┘└──────────┘┴└──────────────┘┴└──────────────┘
doc ───┘ └───┘ ┴└──────────────┘┴
txt ───┘ └───┘ ┴ ┴
par ───┘ └───┘ ┴ ┴
pid ───┘ └───┘ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
208 have I3 : ∀x y, is_closed {f : Cb α β | f (x, y) = f (y, x)} :=
id └───────┘ ┴ └┘ ┴ ┴ ┴
src └────────┘ └─┘ ┴└───────┘┴┴└──┘└┘┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴┴ └┘ └─────
typ └────────┘ └─┘ ┴└───────┘┴┴└──┘└┘┴┴┴┴└─┘ ┴ └┘ └┘ ┴ ┴┴ └┘ └─────
doc └────────┘ └─┘ ┴└───────┘┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └─────
txt └────────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └─────
par └────────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └─────
pid └─────┘└─┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘└───
st ──────────────────────────────────────────────────────────────────
209 λx y, is_closed_eq continuous_evalx continuous_evalx,
id └──────────┘ └──────────────┘
src ───┘ └───┘└──────────┘┴ ┴└──────────────┘
typ ───┘ └───┘└──────────┘┴ ┴└──────────────┘
doc ───┘ └───┘ ┴ ┴└──────────────┘
txt ───┘ └───┘ ┴ ┴
par ───┘ └───┘ ┴ ┴
pid ───┘ └───┘ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
210 have I4 : ∀x y z, is_closed {f : Cb α β | f (x, z) ≤ f (x, y) + f (y, z)} :=
id └───────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └────────┘ └───┘ ┴└───────┘┴┴└──┘└┘┴ ┴ └─┘ ┴ └┘ └┘┴┴ ┴ └┘ └┘┴┴ ┴┴ └┘ └─────
typ └────────┘ └───┘ ┴└───────┘┴┴└──┘└┘┴┴┴┴└─┘ ┴ └┘ └┘┴┴ ┴ └┘ └┘┴┴ ┴┴ └┘ └─────
doc └────────┘ └───┘ ┴└───────┘┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └─────
txt └────────┘ └───┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └─────
par └────────┘ └───┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └─────
pid └─────┘└─┘ └───┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └┘└───
st ───────────────────────────────────────────────────────────────────────────────
211 λx y z, is_closed_le continuous_evalx (continuous_evalx.add continuous_evalx),
id └──────────┘ └──────────────────┘ └──────────────┘
src ───┘ └─────┘└──────────┘┴ ┴ └──────────────────┘┴└──────────────┘┴
typ ───┘ └─────┘└──────────┘┴ ┴ └──────────────────┘┴└──────────────┘┴
doc ───┘ └─────┘ ┴ ┴ ┴└──────────────┘┴
txt ───┘ └─────┘ ┴ ┴ ┴ ┴
par ───┘ └─────┘ ┴ ┴ ┴ ┴
pid ───┘ └─────┘ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────┘└─
212 have I5 : ∀x, is_closed {f : Cb α β | f (x, x) = 0} :=
id └───────┘ ┴ └┘ ┴ ┴ ┴
src └────────┘ ┴ ┴└───────┘┴┴└──┘└┘┴ ┴ └─┘ ┴┴ └┘ └┘ └──────
typ └────────┘ ┴ ┴└───────┘┴┴└──┘└┘┴┴┴┴└─┘ ┴┴ └┘ └┘ └──────
doc └────────┘ ┴ ┴└───────┘┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ └──────
txt └────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ └──────
par └────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ └──────
pid └─────┘└─┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ └─┘└───
st ─────────────────────────────────────────────────────────
213 λx, is_closed_eq continuous_evalx continuous_const,
id └──────────┘ └──────────────┘ └──────────────┘
src ───┘ └─┘└──────────┘┴└──────────────┘┴└──────────────┘
typ ───┘ └─┘└──────────┘┴└──────────────┘┴└──────────────┘
doc ───┘ └─┘ ┴└──────────────┘┴
txt ───┘ └─┘ ┴ ┴
par ───┘ └─┘ ┴ ┴
pid ───┘ └─┘ ┴ ┴
st ─────────────────────────────────────────────────────┘└─
214 have I6 : ∀x y, is_closed {f : Cb α β | f (x, y) ≤ max_var α β} :=
id └───────┘ ┴ └┘ ┴ └─────┘ ┴ ┴
src └────────┘ └─┘ ┴└───────┘┴┴└──┘└┘┴ ┴ └─┘ ┴┴ └┘ └┘ ┴└─────┘┴ ┴ └────
typ └────────┘ └─┘ ┴└───────┘┴┴└──┘└┘┴ ┴ └─┘ ┴┴ └┘ └┘ ┴└─────┘┴┴┴┴└────
doc └────────┘ └─┘ ┴└───────┘┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ └────
txt └────────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ └────
par └────────┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ └────
pid └─────┘└─┘ └─┘ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴└───
st ─────────────────────────────────────────────────────────────────────
215 λx y, is_closed_le continuous_evalx continuous_const,
id └──────────┘ └──────────────┘ └──────────────┘
src ───┘ └───┘└──────────┘┴└──────────────┘┴└──────────────┘
typ ───┘ └───┘└──────────┘┴└──────────────┘┴└──────────────┘
doc ───┘ └───┘ ┴└──────────────┘┴
txt ───┘ └───┘ ┴ ┴
par ───┘ └───┘ ┴ ┴
pid ───┘ └───┘ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
216 have : candidates_b α β = (⋂x y, {f : Cb α β | f ((@inl α β x), (@inl α β y)) = dist x y})
id └──────────┘ └─┘
src └─────┘└──────────┘┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ └─┘┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
typ └─────┘└──────────┘┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ └─┘┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
doc └─────┘└──────────┘┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
txt └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
par └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
pid └───┘└┘ ┴ ┴ ┴ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
st ─────────────────────────────────────────────────────────────────────────────────────────────
217 ∩ (⋂x y, {f : Cb α β | f ((@inr α β x), (@inr α β y)) = dist x y})
id ┴ └─┘ └──┘
src ──────────────┘┴┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ └─┘┴ ┴ ┴ └─┘ ┴└──┘┴ ┴ └──
typ ──────────────┘┴┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ └─┘┴ ┴ ┴ └─┘ ┴└──┘┴ ┴ └──
doc ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
txt ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
par ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
pid ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
st ──────────────────────────────────────────────────────────────────────────────────
218 ∩ (⋂x y, {f : Cb α β | f (x, y) = f (y, x)})
src ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └───
typ ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └───
doc ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └───
txt ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └───
par ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └───
pid ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └───
st ────────────────────────────────────────────────────────────
219 ∩ (⋂x y z, {f : Cb α β | f (x, z) ≤ f (x, y) + f (y, z)})
src ──────────────┘ ┴ └───┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └───
typ ──────────────┘ ┴ └───┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └───
doc ──────────────┘ ┴ └───┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └───
txt ──────────────┘ ┴ └───┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └───
par ──────────────┘ ┴ └───┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └───
pid ──────────────┘ ┴ └───┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └───
st ─────────────────────────────────────────────────────────────────────────
220 ∩ (⋂x, {f : Cb α β | f (x, x) = 0})
id ┴ ┴
src ──────────────┘ ┴ ┴┴┴┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ └────
typ ──────────────┘ ┴ ┴┴┴┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ └────
doc ──────────────┘ ┴ ┴┴┴┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ └────
txt ──────────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ └────
par ──────────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ └────
pid ──────────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ └────
st ───────────────────────────────────────────────────
221 ∩ (⋂x y, {f : Cb α β | f (x, y) ≤ max_var α β}) :=
id ┴ └┘ ┴ └─────┘ ┴ ┴
src ──────────────┘ ┴ └─┘ ┴┴└──┘└┘┴ ┴ └─┘ ┴┴ └┘ └┘ ┴└─────┘┴ ┴ └─────
typ ──────────────┘ ┴ └─┘ ┴┴└──┘└┘┴ ┴ └─┘ ┴┴ └┘ └┘ ┴└─────┘┴┴┴┴└─────
doc ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ └─────
txt ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ └─────
par ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ └─────
pid ──────────────┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘└───
st ──────────────────────────────────────────────────────────────────
222 begin ext, unfold candidates_b, unfold candidates, simp [-sum.forall], refl end,
src ───┘ ┴└─┘└┘└─────────────────┘└┘└───────────────┘└┘└────────────────┘└┘└───┘└─┘
typ ───┘ ┴└─┘└┘└─────────────────┘└┘└───────────────┘└┘└────────────────┘└┘└───┘└─┘
doc ───┘ ┴└─┘└┘└─────────────────┘└┘└───────────────┘└┘└────────────────┘└┘└───┘└─┘
txt ───┘ ┴└─┘└┘└─────────────────┘└┘└───────────────┘└┘└────────────────┘└┘└───┘└─┘
par ───┘ ┴└─┘└┘└─────────────────┘└┘└───────────────┘└┘└────────────────┘└┘└───┘└─┘
pid ───┘ └────────────────────────────────────────────────────────────────────────┘
st ───┘└───────┘└───────────────────┘└─────────────────┘└──────────────────┘└─────┘└─┘└─
223 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
224 repeat { apply is_closed_inter _ _
id └─────────────┘
src └───────┘└────┘└─────────────┘└────
typ └───────┘└────┘└─────────────┘└────
doc └───────┘└────┘ └────
txt └───────┘└────┘ └────
par └───────┘└────┘ └────
pid └───────┘ └────
st ─────────────────────────────────────
225 <|> apply is_closed_Inter _
id └─────────────┘
src ──────┘└──┘└────┘└─────────────┘└──
typ ──────┘└──┘└────┘└─────────────┘└──
doc ──────┘└──┘└────┘ └──
txt ──────┘└──┘└────┘ └──
par ──────┘└──┘└────┘ └──
pid ────────────────┘ └──
st ───────────────────────────────────
226 <|> apply I1 _ _
id └┘
src ──────┘└──┘└────┘ └────
typ ──────┘└──┘└────┘└┘└────
doc ──────┘└──┘└────┘ └────
txt ──────┘└──┘└────┘ └────
par ──────┘└──┘└────┘ └────
pid ────────────────┘ └────
st ────────────────────────
227 <|> apply I2 _ _
id └┘
src ──────┘└──┘└────┘ └────
typ ──────┘└──┘└────┘└┘└────
doc ──────┘└──┘└────┘ └────
txt ──────┘└──┘└────┘ └────
par ──────┘└──┘└────┘ └────
pid ────────────────┘ └────
st ────────────────────────
228 <|> apply I3 _ _
id └┘
src ──────┘└──┘└────┘ └────
typ ──────┘└──┘└────┘└┘└────
doc ──────┘└──┘└────┘ └────
txt ──────┘└──┘└────┘ └────
par ──────┘└──┘└────┘ └────
pid ────────────────┘ └────
st ────────────────────────
229 <|> apply I4 _ _ _
id └┘
src ──────┘└──┘└────┘ └──────
typ ──────┘└──┘└────┘└┘└──────
doc ──────┘└──┘└────┘ └──────
txt ──────┘└──┘└────┘ └──────
par ──────┘└──┘└────┘ └──────
pid ────────────────┘ └──────
st ──────────────────────────
230 <|> apply I5 _
id └┘
src ──────┘└──┘└────┘ └──
typ ──────┘└──┘└────┘└┘└──
doc ──────┘└──┘└────┘ └──
txt ──────┘└──┘└────┘ └──
par ──────┘└──┘└────┘ └──
pid ────────────────┘ └──
st ──────────────────────
231 <|> apply I6 _ _
id └┘
src ──────┘└──┘└────┘ └────
typ ──────┘└──┘└────┘└┘└────
doc ──────┘└──┘└────┘ └────
txt ──────┘└──┘└────┘ └────
par ──────┘└──┘└────┘ └────
pid ────────────────┘ └────
st ────────────────────────
232 <|> assume x },
src ──────┘└──┘└───────┘
typ ──────┘└──┘└───────┘
doc ──────┘└──┘└───────┘
txt ──────┘└──┘└───────┘
par ──────┘└──┘└───────┘
pid ───────────────────┘
st ───────────────────┘
233 end
st └─┘
234
235 /-- Compactness of candidates (in bounded_continuous_functions) follows -/
236 private lemma compact_candidates_b : compact (candidates_b α β) :=
id ┴ ┴
typ ┴ ┴
237 begin
238 refine arzela_ascoli₂ (Icc 0 (max_var α β)) compact_Icc (candidates_b α β) closed_candidates_b _ _,
239 { rintros f ⟨x1, x2⟩ hf,
240 simp only [set.mem_Icc],
241 exact ⟨candidates_nonneg hf, candidates_le_max_var hf⟩ },
st └┘
242 { refine equicontinuous_of_continuity_modulus (λt, 2 * max_var α β * t) _ _ _,
id ┴ ┴ ┴
typ ┴ ┴ ┴
243 { have : tendsto (λ (t : ℝ), 2 * (max_var α β : ℝ) * t) (𝓝 0) (𝓝 (2 * max_var α β * 0)) :=
id ┴ ┴
typ ┴ ┴
244 tendsto_const_nhds.mul tendsto_id,
245 simpa using this },
st └┘
246 { assume x y f hf,
247 exact candidates_lipschitz hf _ _ } }
st └───
248 end
st ──┘
249
250 /-- We will then choose the candidate minimizing the Hausdorff distance. Except that we are not
251 in a metric space setting, so we need to define our custom version of Hausdorff distance,
252 called HD, and prove its basic properties. -/
253 def HD (f : Cb α β) := max (supr (λx:α, infi (λy:β, f (inl x, inr y))))
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
254 (supr (λy:β, infi (λx:α, f (inl x, inr y))))
id ┴ ┴
typ ┴ ┴
255
256 /- We will show that HD is continuous on bounded_continuous_functions, to deduce that its
257 minimum on the compact set candidates_b is attained. Since it is defined in terms of
258 infimum and supremum on ℝ, which is only conditionnally complete, we will need all the time
259 to check that the defining sets are bounded below or above. This is done in the next few
260 technical lemmas -/
261
262 lemma HD_below_aux1 {f : Cb α β} (C : ℝ) {x : α} : bdd_below (range (λ (y : β), f (inl x, inr y) + C)) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
263 let ⟨cf, hcf⟩ := (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 in
id └┘
typ └┘
264 ⟨cf + C, forall_range_iff.2 (λi, add_le_add_right ((λx, hcf (mem_range_self x)) _) _)⟩
id ┴ ┴
typ ┴ ┴
265
266 private lemma HD_bound_aux1 (f : Cb α β) (C : ℝ) : bdd_above (range (λ (x : α), infi (λy:β, f (inl x, inr y) + C))) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
267 begin
268 rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).2 with ⟨Cf, hCf⟩,
269 refine ⟨Cf + C, forall_range_iff.2 (λx, _)⟩,
id └┘ ┴ ┴
typ └┘ ┴ ┴
270 calc infi (λy:β, f (inl x, inr y) + C) ≤ f (inl x, inr (default β)) + C :
id ┴ ┴
typ ┴ ┴
271 cinfi_le (HD_below_aux1 C)
id ┴
typ ┴
272 ... ≤ Cf + C : add_le_add ((λx, hCf (mem_range_self x)) _) (le_refl _)
id └┘
typ └┘
273 end
st └─┘
274
275 lemma HD_below_aux2 {f : Cb α β} (C : ℝ) {y : β} : bdd_below (range (λ (x : α), f (inl x, inr y) + C)) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
276 let ⟨cf, hcf⟩ := (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 in
id └┘
typ └┘
277 ⟨cf + C, forall_range_iff.2 (λi, add_le_add_right ((λx, hcf (mem_range_self x)) _) _)⟩
id ┴ ┴
typ ┴ ┴
278
279 private lemma HD_bound_aux2 (f : Cb α β) (C : ℝ) : bdd_above (range (λ (y : β), infi (λx:α, f (inl x, inr y) + C))) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
280 begin
281 rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).2 with ⟨Cf, hCf⟩,
282 refine ⟨Cf + C, forall_range_iff.2 (λy, _)⟩,
id └┘ ┴ ┴
typ └┘ ┴ ┴
283 calc infi (λx:α, f (inl x, inr y) + C) ≤ f (inl (default α), inr y) + C :
id ┴ ┴
typ ┴ ┴
284 cinfi_le (HD_below_aux2 C)
id ┴
typ ┴
285 ... ≤ Cf + C : add_le_add ((λx, hCf (mem_range_self x)) _) (le_refl _)
id └┘
typ └┘
286 end
st └─┘
287
288 /-- Explicit bound on HD (dist). This means that when looking for minimizers it will
289 be sufficient to look for functions with HD(f) bounded by this bound. -/
290 lemma HD_candidates_b_dist_le : HD (candidates_b_dist α β) ≤ diam (univ : set α) + 1 + diam (univ : set β) :=
id ┴ ┴ └┘ ┴ └┘ ┴
src └┘ └┘
typ ┴ ┴ └┘ ┴ └┘ ┴
291 begin
292 refine max_le (csupr_le (λx, _)) (csupr_le (λy, _)),
293 { have A : infi (λy:β, candidates_b_dist α β (inl x, inr y)) ≤ candidates_b_dist α β (inl x, inr (default β)) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
294 cinfi_le (by simpa using HD_below_aux1 0),
295 have B : dist (inl x) (inr (default β)) ≤ diam (univ : set α) + 1 + diam (univ : set β) := calc
id ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ └─┘ ┴
296 dist (inl x) (inr (default β)) = dist x (default α) + 1 + dist (default β) (default β) : rfl
id ┴
typ ┴
297 ... ≤ diam (univ : set α) + 1 + diam (univ : set β) :
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
298 begin
299 apply add_le_add (add_le_add _ (le_refl _)),
300 exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _),
301 exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _)
302 end,
st └─┘
303 exact le_trans A B },
st └┘
304 { have A : infi (λx:α, candidates_b_dist α β (inl x, inr y)) ≤ candidates_b_dist α β (inl (default α), inr y) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
305 cinfi_le (by simpa using HD_below_aux2 0),
306 have B : dist (inl (default α)) (inr y) ≤ diam (univ : set α) + 1 + diam (univ : set β) := calc
id ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ └─┘ ┴
307 dist (inl (default α)) (inr y) = dist (default α) (default α) + 1 + dist (default β) y : rfl
id ┴
typ ┴
308 ... ≤ diam (univ : set α) + 1 + diam (univ : set β) :
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
309 begin
310 apply add_le_add (add_le_add _ (le_refl _)),
311 exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _),
312 exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _)
313 end,
st └─┘
314 exact le_trans A B },
st └┘
315 end
st └─┘
316
317 /- To check that HD is continuous, we check that it is Lipschitz. As HD is a max, we
318 prove separately inequalities controlling the two terms (relying too heavily on copy-paste...) -/
319 private lemma HD_lipschitz_aux1 (f g : Cb α β) :
id ┴ ┴
typ ┴ ┴
320 supr (λx:α, infi (λy:β, f (inl x, inr y))) ≤ supr (λx:α, infi (λy:β, g (inl x, inr y))) + dist f g :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
321 begin
322 rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 with ⟨cg, hcg⟩,
323 have Hcg : ∀x, cg ≤ g x := λx, hcg (mem_range_self x),
id └┘
typ └┘
324 rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 with ⟨cf, hcf⟩,
325 have Hcf : ∀x, cf ≤ f x := λx, hcf (mem_range_self x),
id └┘
typ └┘
326
327 -- prove the inequality but with `dist f g` inside, by using inequalities comparing
328 -- supr to supr and infi to infi
329 have Z : supr (λx:α, infi (λy:β, f (inl x, inr y))) ≤ supr (λx:α, infi (λy:β, g (inl x, inr y) + dist f g)) :=
id ┴ ┴
typ ┴ ┴
330 csupr_le_csupr (HD_bound_aux1 _ (dist f g))
331 (λx, cinfi_le_cinfi ⟨cf, forall_range_iff.2(λi, Hcf _)⟩ (λy, coe_le_coe_add_dist)),
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
332 -- move the `dist f g` out of the infimum and the supremum, arguing that continuous monotone maps
333 -- (here the addition of `dist f g`) preserve infimum and supremum
334 have E1 : ∀x, infi (λy:β, g (inl x, inr y)) + dist f g =
id ┴
typ ┴
335 infi ((λz, z + dist f g) ∘ (λy:β, (g (inl x, inr y)))),
id ┴ ┴
typ ┴ ┴
336 { assume x,
337 refine cinfi_of_cinfi_of_monotone_of_continuous (_ : continuous (λ (z : ℝ), z + dist f g)) _ _,
338 { exact continuous_id.add continuous_const },
st └┘
339 { assume x y hx, simpa },
st └┘
340 { show bdd_below (range (λ (y : β), g (inl x, inr y))),
id ┴ ┴
typ ┴ ┴
341 from ⟨cg, forall_range_iff.2(λi, Hcg _)⟩ } },
id └┘ ┴
typ └┘ ┴
st └──┘
342 have E2 : supr (λx:α, infi (λy:β, g (inl x, inr y))) + dist f g =
343 supr ((λz, z + dist f g) ∘ (λx:α, infi (λy:β, g (inl x, inr y)))),
id ┴ ┴ ┴
typ ┴ ┴ ┴
344 { refine csupr_of_csupr_of_monotone_of_continuous (_ : continuous (λ (z : ℝ), z + dist f g)) _ _,
345 { exact continuous_id.add continuous_const },
st └┘
346 { assume x y hx, simpa },
st └┘
347 { by simpa using HD_bound_aux1 _ 0 } },
st └──┘
348 -- deduce the result from the above two steps
349 simp only [add_comm] at Z,
350 simpa [E2, E1, function.comp]
351 end
st └─┘
352
353 private lemma HD_lipschitz_aux2 (f g : Cb α β) :
id ┴ ┴
typ ┴ ┴
354 supr (λy:β, infi (λx:α, f (inl x, inr y))) ≤ supr (λy:β, infi (λx:α, g (inl x, inr y))) + dist f g :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
355 begin
356 rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 with ⟨cg, hcg⟩,
357 have Hcg : ∀x, cg ≤ g x := λx, hcg (mem_range_self x),
id └┘
typ └┘
358 rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 with ⟨cf, hcf⟩,
359 have Hcf : ∀x, cf ≤ f x := λx, hcf (mem_range_self x),
id └┘
typ └┘
360
361 -- prove the inequality but with `dist f g` inside, by using inequalities comparing
362 -- supr to supr and infi to infi
363 have Z : supr (λy:β, infi (λx:α, f (inl x, inr y))) ≤ supr (λy:β, infi (λx:α, g (inl x, inr y) + dist f g)) :=
id ┴ ┴
typ ┴ ┴
364 csupr_le_csupr (HD_bound_aux2 _ (dist f g))
365 (λy, cinfi_le_cinfi ⟨cf, forall_range_iff.2(λi, Hcf _)⟩ (λy, coe_le_coe_add_dist)),
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
366 -- move the `dist f g` out of the infimum and the supremum, arguing that continuous monotone maps
367 -- (here the addition of `dist f g`) preserve infimum and supremum
368 have E1 : ∀y, infi (λx:α, g (inl x, inr y)) + dist f g =
id ┴
typ ┴
369 infi ((λz, z + dist f g) ∘ (λx:α, (g (inl x, inr y)))),
id ┴ ┴
typ ┴ ┴
370 { assume y,
371 refine cinfi_of_cinfi_of_monotone_of_continuous (_ : continuous (λ (z : ℝ), z + dist f g)) _ _,
372 { exact continuous_id.add continuous_const },
st └┘
373 { assume x y hx, simpa },
st └┘
374 { show bdd_below (range (λx:α, g (inl x, inr y))),
id ┴ ┴
typ ┴ ┴
375 from ⟨cg, forall_range_iff.2(λi, Hcg _)⟩ } },
id └┘ ┴
typ └┘ ┴
st └──┘
376 have E2 : supr (λy:β, infi (λx:α, g (inl x, inr y))) + dist f g =
377 supr ((λz, z + dist f g) ∘ (λy:β, infi (λx:α, g (inl x, inr y)))),
id ┴ ┴ ┴
typ ┴ ┴ ┴
378 { refine csupr_of_csupr_of_monotone_of_continuous (_ : continuous (λ (z : ℝ), z + dist f g)) _ _,
379 { exact continuous_id.add continuous_const },
st └┘
380 { assume x y hx, simpa },
st └┘
381 { by simpa using HD_bound_aux2 _ 0 } },
st └──┘
382 -- deduce the result from the above two steps
383 simp only [add_comm] at Z,
384 simpa [E2, E1, function.comp]
385 end
st └─┘
386
387 private lemma HD_lipschitz_aux3 (f g : Cb α β) : HD f ≤ HD g + dist f g :=
id ┴ ┴
typ ┴ ┴
388 max_le (le_trans (HD_lipschitz_aux1 f g) (add_le_add_right (le_max_left _ _) _))
389 (le_trans (HD_lipschitz_aux2 f g) (add_le_add_right (le_max_right _ _) _))
390
391 /-- Conclude that HD, being Lipschitz, is continuous -/
392 private lemma HD_continuous : continuous (HD : Cb α β → ℝ) :=
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
393 lipschitz_with.to_continuous (lipschitz_with.one_of_le_add HD_lipschitz_aux3)
394
395 end constructions --section
396
397 section consequences
398 variables (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β]
id └┘ ┴ └──┘ ┴└──────────┘ └───────────┘ └──────┘ └──────────┘ └───────────┘ └──────┘
src └──────────┘ └───────────┘ └──────┘ └──────────┘ └───────────┘ └──────┘
typ └┘ ┴ └──┘ ┴└──────────┘ └───────────┘ └──────┘ └──────────┘ └───────────┘ └──────┘
doc └──────────┘ └───────────┘ └──────────┘ └───────────┘
399
400 /- Now that we have proved that the set of candidates is compact, and that HD is continuous,
401 we can finally select a candidate minimizing HD. This will be the candidate realizing the
402 optimal coupling. -/
403 private lemma exists_minimizer : ∃f ∈ candidates_b α β, ∀g ∈ candidates_b α β, HD f ≤ HD g :=
id ┴┴ └──────────┘ ┴ ┴┴ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ └──────────┘ ┴ ┴ └──────────┘ └┘ ┴ └┘
typ ┴┴ └──────────┘ ┴ ┴┴ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └──────────┘ └──────────┘ └┘ └┘
404 compact_candidates_b.exists_forall_le candidates_b_nonempty HD_continuous.continuous_on
id └──────────────────┘└───────────────┘ └───────────────────┘ └───────────┘└────────────┘
src └──────────────────┘└───────────────┘ └───────────────────┘ └───────────┘└────────────┘
typ └──────────────────┘└───────────────┘ └───────────────────┘ └───────────┘└────────────┘
doc └──────────────────┘└───────────────┘ └───────────┘
405
406 private definition optimal_GH_dist : Cb α β := classical.some (exists_minimizer α β)
id └┘ ┴ ┴ └────────────┘ └──────────────┘ ┴ ┴
src └┘ └────────────┘ └──────────────┘
typ └┘ ┴ ┴ └────────────┘ └──────────────┘ ┴ ┴
407
408 private lemma optimal_GH_dist_mem_candidates_b : optimal_GH_dist α β ∈ candidates_b α β :=
id └─────────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴
src └─────────────┘ ┴ └──────────┘
typ └─────────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘
409 by cases (classical.some_spec (exists_minimizer α β)); assumption
id └─────────────────┘ └──────────────┘ ┴ ┴
src └────┘ └─────────────────┘┴ └──────────────┘┴ ┴ └┘ └──────────
typ └────┘ └─────────────────┘┴ └──────────────┘┴┴┴┴└┘ └──────────
doc └────┘ ┴ ┴ ┴ └┘ └──────────
txt └────┘ ┴ ┴ ┴ └┘ └──────────
par └────┘ ┴ ┴ ┴ └┘ └──────────
pid ┴ ┴ ┴ ┴ └┘ └
st └───────────────────────────────────────────────────────────────
410
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
411 private lemma HD_optimal_GH_dist_le (g : Cb α β) (hg : g ∈ candidates_b α β) : HD (optimal_GH_dist α β) ≤ HD g :=
id └┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └┘ └─────────────┘ ┴ ┴ ┴ └┘ ┴
src └┘ ┴ └──────────┘ └┘ └─────────────┘ ┴ └┘
typ └┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └┘ └─────────────┘ ┴ ┴ ┴ └┘ ┴
doc └──────────┘ └┘ └┘
412 let ⟨Z1, Z2⟩ := classical.some_spec (exists_minimizer α β) in Z2 g hg
id └─┘ └┘ └─────────────────┘ └──────────────┘ ┴ ┴ ┴ └┘
src └─────────────────┘ └──────────────┘
typ └─┘ └┘ └─────────────────┘ └──────────────┘ ┴ ┴ ┴ └┘
413
414 /-- With the optimal candidate, construct a premetric space structure on α ⊕ β, on which the
415 predistance is given by the candidate. Then, we will identify points at 0 predistance
416 to obtain a genuine metric space -/
417 def premetric_optimal_GH_dist : premetric_space (α ⊕ β) :=
id └─────────────┘ ┴ ┴ ┴
src └─────────────┘ ┴
typ └─────────────┘ ┴ ┴ ┴
418 { dist := λp q, optimal_GH_dist α β (p, q),
id ┴ ┴ └─────────────┘ ┴ ┴ ┴┴ ┴
src └─────────────┘ ┴
typ ┴ ┴ └─────────────┘ ┴ ┴ ┴┴ ┴
419 dist_self := λx, candidates_refl (optimal_GH_dist_mem_candidates_b α β),
id ┴ └─────────────┘ └──────────────────────────────┘ ┴ ┴
src └─────────────┘ └──────────────────────────────┘
typ ┴ └─────────────┘ └──────────────────────────────┘ ┴ ┴
420 dist_comm := λx y, candidates_symm (optimal_GH_dist_mem_candidates_b α β),
id ┴ ┴ └─────────────┘ └──────────────────────────────┘ ┴ ┴
src └─────────────┘ └──────────────────────────────┘
typ ┴ ┴ └─────────────┘ └──────────────────────────────┘ ┴ ┴
421 dist_triangle := λx y z, candidates_triangle (optimal_GH_dist_mem_candidates_b α β) }
id ┴ ┴ ┴ └─────────────────┘ └──────────────────────────────┘ ┴ ┴
src └─────────────────┘ └──────────────────────────────┘
typ ┴ ┴ ┴ └─────────────────┘ └──────────────────────────────┘ ┴ ┴
422
423 local attribute [instance] premetric_optimal_GH_dist premetric.dist_setoid
id └───────────────────────┘ └───────────────────┘
src └───────────────────────┘ └───────────────────┘
typ └───────────────────────┘ └───────────────────┘
doc └───────────────────────┘ └───────────────────┘
424
425 /-- A metric space which realizes the optimal coupling between α and β -/
426 @[derive [metric_space]] definition optimal_GH_coupling : Type* :=
id └──────────┘
src └──────────┘
typ └──────────┘
doc └────┘ └──────────┘
427 premetric.metric_quot (α ⊕ β)
id └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘ ┴
typ └───────────────────┘ ┴ ┴ ┴
doc └───────────────────┘
428
429 /-- Injection of α in the optimal coupling between α and β -/
430 def optimal_GH_injl (x : α) : optimal_GH_coupling α β := ⟦inl x⟧
id ┴ └─────────────────┘ ┴ ┴ ┴└─┘ ┴┴
src └─────────────────┘ ┴└─┘ ┴
typ ┴ └─────────────────┘ ┴ ┴ ┴└─┘ ┴┴
doc └─────────────────┘
431
432 /-- The injection of α in the optimal coupling between α and β is an isometry. -/
433 lemma isometry_optimal_GH_injl : isometry (optimal_GH_injl α β) :=
id └──────┘ └─────────────┘ ┴ ┴
src └──────┘ └─────────────┘
typ └──────┘ └─────────────┘ ┴ ┴
doc └──────┘ └─────────────┘
434 begin
st └─────
435 refine isometry_emetric_iff_metric.2 (λx y, _),
id └─────────────────────────┘
src └─────┘└─────────────────────────┘└─┘ └─────┘
typ └─────┘└─────────────────────────┘└─┘ └─────┘
doc └─────┘└─────────────────────────┘└─┘ └─────┘
txt └─────┘ └─┘ └─────┘
par └─────┘ └─┘ └─────┘
pid ┴ └─┘ └─────┘
st ───────────────────────────────────────────────┘└─
436 change dist ⟦inl x⟧ ⟦inl y⟧ = dist x y,
id ┴ ┴ └─┘ ┴ └──┘ ┴ ┴
src └─────┘ ┴┴ ┴ ┴┴ └─┘┴ ┴┴┴└──┘┴ ┴
typ └─────┘ ┴┴ ┴ ┴┴ └─┘┴ ┴┴┴└──┘┴┴┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────┘└─
437 exact candidates_dist_inl (optimal_GH_dist_mem_candidates_b α β) _ _,
id └─────────────────┘ └──────────────────────────────┘ ┴ ┴
src └────┘└─────────────────┘┴ └──────────────────────────────┘┴ ┴ └───┘
typ └────┘└─────────────────┘┴ └──────────────────────────────┘┴┴┴┴└───┘
doc └────┘ ┴ ┴ ┴ └───┘
txt └────┘ ┴ ┴ ┴ └───┘
par └────┘ ┴ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴ └───┘
st ─────────────────────────────────────────────────────────────────────┘└─
438 end
st ──┘
439
440 /-- Injection of β in the optimal coupling between α and β -/
441 def optimal_GH_injr (y : β) : optimal_GH_coupling α β := ⟦inr y⟧
id ┴ └─────────────────┘ ┴ ┴ ┴└─┘ ┴┴
src └─────────────────┘ ┴└─┘ ┴
typ ┴ └─────────────────┘ ┴ ┴ ┴└─┘ ┴┴
doc └─────────────────┘
442
443 /-- The injection of β in the optimal coupling between α and β is an isometry. -/
444 lemma isometry_optimal_GH_injr : isometry (optimal_GH_injr α β) :=
id └──────┘ └─────────────┘ ┴ ┴
src └──────┘ └─────────────┘
typ └──────┘ └─────────────┘ ┴ ┴
doc └──────┘ └─────────────┘
445 begin
st └─────
446 refine isometry_emetric_iff_metric.2 (λx y, _),
id └─────────────────────────┘
src └─────┘└─────────────────────────┘└─┘ └─────┘
typ └─────┘└─────────────────────────┘└─┘ └─────┘
doc └─────┘└─────────────────────────┘└─┘ └─────┘
txt └─────┘ └─┘ └─────┘
par └─────┘ └─┘ └─────┘
pid ┴ └─┘ └─────┘
st ───────────────────────────────────────────────┘└─
447 change dist ⟦inr x⟧ ⟦inr y⟧ = dist x y,
id ┴ ┴ └─┘ ┴ └──┘ ┴ ┴
src └─────┘ ┴┴ ┴ ┴┴ └─┘┴ ┴┴┴└──┘┴ ┴
typ └─────┘ ┴┴ ┴ ┴┴ └─┘┴ ┴┴┴└──┘┴┴┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────┘└─
448 exact candidates_dist_inr (optimal_GH_dist_mem_candidates_b α β) _ _,
id └─────────────────┘ └──────────────────────────────┘ ┴ ┴
src └────┘└─────────────────┘┴ └──────────────────────────────┘┴ ┴ └───┘
typ └────┘└─────────────────┘┴ └──────────────────────────────┘┴┴┴┴└───┘
doc └────┘ ┴ ┴ ┴ └───┘
txt └────┘ ┴ ┴ ┴ └───┘
par └────┘ ┴ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴ └───┘
st ─────────────────────────────────────────────────────────────────────┘└─
449 end
st ──┘
450
451 /-- The optimal coupling between two compact spaces α and β is still a compact space -/
452 instance compact_space_optimal_GH_coupling : compact_space (optimal_GH_coupling α β) :=
id └───────────┘ └─────────────────┘ ┴ ┴
src └───────────┘ └─────────────────┘
typ └───────────┘ └─────────────────┘ ┴ ┴
doc └───────────┘ └─────────────────┘
453 ⟨begin
st └─────
454 have : (univ : set (optimal_GH_coupling α β)) =
id └─┘ └─────────────────┘ ┴
src └─────┘ └─┘└─┘┴ └─────────────────┘┴ ┴ └─┘┴└
typ └─────┘ └─┘└─┘┴ └─────────────────┘┴ ┴ └─┘┴└
doc └─────┘ └─┘ ┴ └─────────────────┘┴ ┴ └─┘ └
txt └─────┘ └─┘ ┴ ┴ ┴ └─┘ └
par └─────┘ └─┘ ┴ ┴ ┴ └─┘ └
pid └───┘└┘ └─┘ ┴ ┴ ┴ └─┘ └
st ──────────────────────────────────────────────────
455 (optimal_GH_injl α β '' univ) ∪ (optimal_GH_injr α β '' univ),
id └─────────────┘ └┘ ┴ └─────────────┘ ┴ ┴ └──┘
src ──────────┘ └─────────────┘┴ ┴ ┴└┘┴ └┘┴┴ └─────────────┘┴ ┴ ┴ ┴└──┘┴
typ ──────────┘ └─────────────┘┴ ┴ ┴└┘┴ └┘┴┴ └─────────────┘┴┴┴┴┴ ┴└──┘┴
doc ──────────┘ └─────────────┘┴ ┴ ┴ ┴ └┘ ┴ └─────────────┘┴ ┴ ┴ ┴ ┴
txt ──────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
par ──────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ──────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
456 { refine subset.antisymm (λxc hxc, _) (subset_univ _),
id └─────────────┘ └─────────┘
src └─────┘└─────────────┘┴ └─────────┘ └─────────┘└─┘
typ └─────┘└─────────────┘┴ └─────────┘ └─────────┘└─┘
doc └─────┘ ┴ └─────────┘ └─┘
txt └─────┘ ┴ └─────────┘ └─┘
par └─────┘ ┴ └─────────┘ └─┘
pid ┴ ┴ └─────────┘ └─┘
st ───┘└─────────────────────────────────────────────────┘└─
457 rcases quotient.exists_rep xc with ⟨x, hx⟩,
id └─────────────────┘ └┘
src └─────┘└─────────────────┘┴ └───────────┘
typ └─────┘└─────────────────┘┴└┘└───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ─────────────────────────────────────────────┘└─
458 cases x; rw ← hx,
id ┴ └┘
src └────┘ └───┘
typ └────┘┴ └───┘└┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └─┘
st ───────────────────┘ └
459 { have : ⟦inl x⟧ = optimal_GH_injl α β x := rfl,
id ┴└─┘ ┴ └─────────────┘ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ ┴└─┘┴ ┴ └─────────────┘ ┴ ┴└─┘
typ ┴ ┴ ┴ ┴└─┘┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴└─┘
doc ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴
txt ┴ ┴ ┴ ┴ ┴ ┴
par ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ─────┘ ┴ ┴ ┴ └─────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴ └──┘└─
460 rw this,
id └─┘
src ┴ ┴
typ ┴ ┴ └─┘
doc ┴ ┴
txt ┴ ┴
par ┴ ┴
pid ┴
st ──────┘ ┴ └─┘ ┴
461 exact mem_union_left _ (mem_image_of_mem _ (mem_univ _)) },
id ┴ ┴ ┴ └────────────┘ └──────────────┘ └──────┘
src └────┘└────────────┘└┘ └──────────────┘ ┴ └──────┘└───┘
typ └────┘└────────────┘└┘ └──────────────┘ ┴ └──────┘└───┘
doc └────┘ └┘ ┴ └───┘
txt ┴ ┴ ┴ └┘ ┴ └───┘
par ┴ ┴ ┴ └┘ ┴ └───┘
pid ┴ └┘ ┴ └──┘┴
st ┴ ┴ └─────┘ └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴ └─────┘ └───┘ ┴ ┴ └──────────┘┴ └
462 { have : ⟦inr x⟧ = optimal_GH_injr α β x := rfl,
id └─┘ └─────────────┘ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ └─┘┴ └─────────────┘ ┴ ┴└─┘
typ ┴ ┴ ┴ └─┘┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴└─┘
doc ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴
txt ┴ ┴ ┴ ┴ ┴ ┴
par ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ─────┘ ┴ ┴ ┴ └─────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴ └──┘└─
463 rw this,
id └─┘
src ┴ ┴
typ ┴ ┴ └─┘
doc ┴ ┴
txt ┴ ┴
par ┴ ┴
pid ┴
st ──────┘ ┴ └─┘ ┴
464 exact mem_union_right _ (mem_image_of_mem _ (mem_univ _)) } },
id ┴ ┴ ┴ └─────────────┘ └──────────────┘ └──────┘
src └────┘└─────────────┘└─┘ └──────────────┘└─┘ └──────┘┴ ┴ ┴
typ └────┘└─────────────┘└─┘ └──────────────┘└─┘ └──────┘┴ ┴ ┴
doc └────┘ └─┘ └─┘ ┴ ┴ ┴
txt ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴
par ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴
pid ┴ └─┘ └─┘ ┴ ┴ ┴
st ┴ ┴ └─────┘ └─────┘ └─┘ └─────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘
465 rw this,
id ┴ └──┘
src ┴
typ ┴ └──┘
doc ┴
st ┴ ┴ └──┘ ┴
466 exact (compact_univ.image (isometry_optimal_GH_injl α β).continuous).union
id ┴ ┴ ┴ └──────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ └──────────────────────┘┴ ┴ ┴┴┴┴┴┴┴┴┴┴┴ ┴┴┴┴┴┴┴
typ └────┘ ┴ └──────────────────────┘┴ ┴ ┴┴┴┴┴┴┴┴┴┴┴ ┴┴┴┴┴┴┴
doc └────┘ ┴ └──────────────────────┘┴ ┴ ┴┴┴┴┴┴┴┴┴┴┴ ┴ ┴ ┴ ┴
txt ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
467 (compact_univ.image (isometry_optimal_GH_injr α β).continuous)
id └────────────────┘ └──────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └────────────────┘ └──────────────────────┘ ┴┴┴┴┴┴┴┴┴┴┴ ┴
typ ┴ ┴ └────────────────┘ └──────────────────────┘ ┴ ┴ ┴┴┴┴┴┴┴┴┴┴┴ ┴
doc ┴ ┴ └──────────────────────┘ ┴┴┴┴┴┴┴┴┴┴┴ ┴
txt ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
468 end⟩
st └─┘
469
470 /-- For any candidate f, HD(f) is larger than or equal to the Hausdorff distance in the
471 optimal coupling. This follows from the fact that HD of the optimal candidate is exactly
472 the Hausdorff distance in the optimal coupling, although we only prove here the inequality
473 we need. -/
474 lemma Hausdorff_dist_optimal_le_HD {f} (h : f ∈ candidates_b α β) :
id ┴ ┴ └──────────┘ ┴ ┴
src ┴ └──────────┘
typ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘
475 Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) ≤ HD f :=
id └────────────┘ └───┘ └─────────────┘ ┴ ┴ └───┘ └─────────────┘ ┴ ┴ ┴ └┘ ┴
src └────────────┘ └───┘ └─────────────┘ └───┘ └─────────────┘ ┴ └┘
typ └────────────┘ └───┘ └─────────────┘ ┴ ┴ └───┘ └─────────────┘ ┴ ┴ ┴ └┘ ┴
doc └────────────┘ └───┘ └─────────────┘ └───┘ └─────────────┘ └┘
476 begin
st └───┘
477 refine le_trans (le_of_forall_le_of_dense (λr hr, _)) (HD_optimal_GH_dist_le α β f h),
id └──────┘ └──────────────────────┘ └───────────────────┘ ┴ ┴ ┴ ┴
src └─────┘└──────┘┴ └──────────────────────┘┴ └────────┘ └───────────────────┘┴ ┴ ┴ ┴ ┴
typ └─────┘└──────┘┴ └──────────────────────┘┴ └────────┘ └───────────────────┘┴┴┴┴┴┴┴┴┴
doc └─────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ ┴
st └─────────────────────────────────────────────────────────────────────────────────────┘
478 have A : ∀ x ∈ range (optimal_GH_injl α β), ∃ y ∈ range (optimal_GH_injr α β), dist x y ≤ r,
id ┴ ┴ ┴
typ ┴ ┴ ┴
479 { assume x hx,
480 rcases mem_range.1 hx with ⟨z, hz⟩,
481 rw ← hz,
482 have I1 : supr (λx:α, infi (λy:β, optimal_GH_dist α β (inl x, inr y))) < r :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
483 lt_of_le_of_lt (le_max_left _ _) hr,
484 have I2 : infi (λy:β, optimal_GH_dist α β (inl z, inr y)) ≤
id ┴
typ ┴
485 supr (λx:α, infi (λy:β, optimal_GH_dist α β (inl x, inr y))) :=
id ┴ ┴
typ ┴ ┴
486 le_cSup (by simpa using HD_bound_aux1 _ 0) (mem_range_self _),
487 have I : infi (λy:β, optimal_GH_dist α β (inl z, inr y)) < r := lt_of_le_of_lt I2 I1,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
488 rcases exists_lt_of_cInf_lt (range_nonempty _) I with ⟨r', r'range, hr'⟩,
489 rcases mem_range.1 r'range with ⟨z', hz'⟩,
490 existsi [optimal_GH_injr α β z', mem_range_self _],
id ┴ ┴ └┘
typ ┴ ┴ └┘
491 have : (optimal_GH_dist α β) (inl z, inr z') ≤ r := begin rw hz', exact le_of_lt hr' end,
id ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ └┘ ┴
st └─┘
492 exact this },
st └┘
493 refine Hausdorff_dist_le_of_mem_dist _ A _,
494 { rcases exists_mem_of_nonempty α with ⟨xα, _⟩,
id ┴
typ ┴
495 have : optimal_GH_injl α β xα ∈ range (optimal_GH_injl α β) := mem_range_self _,
id └┘ ┴ ┴
typ └┘ ┴ ┴
496 rcases A _ this with ⟨y, yrange, hy⟩,
497 exact le_trans dist_nonneg hy },
st └┘
498 { assume y hy,
499 rcases mem_range.1 hy with ⟨z, hz⟩,
500 rw ← hz,
501 have I1 : supr (λy:β, infi (λx:α, optimal_GH_dist α β (inl x, inr y))) < r :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
502 lt_of_le_of_lt (le_max_right _ _) hr,
503 have I2 : infi (λx:α, optimal_GH_dist α β (inl x, inr z)) ≤
id ┴
typ ┴
504 supr (λy:β, infi (λx:α, optimal_GH_dist α β (inl x, inr y))) :=
id ┴ ┴
typ ┴ ┴
505 le_cSup (by simpa using HD_bound_aux2 _ 0) (mem_range_self _),
506 have I : infi (λx:α, optimal_GH_dist α β (inl x, inr z)) < r := lt_of_le_of_lt I2 I1,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
507 rcases exists_lt_of_cInf_lt (range_nonempty _) I with ⟨r', r'range, hr'⟩,
508 rcases mem_range.1 r'range with ⟨z', hz'⟩,
509 existsi [optimal_GH_injl α β z', mem_range_self _],
id ┴ ┴ └┘
typ ┴ ┴ └┘
510 have : (optimal_GH_dist α β) (inl z', inr z) ≤ r := begin rw hz', exact le_of_lt hr' end,
id ┴ ┴ └┘ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴
st └─┘
511 rw dist_comm,
512 exact this }
st └─
513 end
st ──┘
514
515 end consequences
516 /- We are done with the construction of the optimal coupling -/
517 end Gromov_Hausdorff_realized
518
519 end Gromov_Hausdorff